\begin{tabbing}
$\forall$${\it es}$:ES, $x$, $i$:Id, $T$:Type.
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ $=$ $y$ $\in$ $T$))
\\[0ex]$\Rightarrow$ vartype($i$;$x$) $\subseteq\rho$ $T$
\\[0ex]$\Rightarrow$ \=$\forall$${\it e'}$@$i$.\+
\\[0ex]($\forall$$e$$<$${\it e'}$. ($x$ when $e$) $=$ ($x$ when ${\it e'}$) $\in$ $T$)
\\[0ex]$\vee$ (\=$\exists$$e$:E.\+
\\[0ex]($e$ $<$loc ${\it e'}$)
\\[0ex]\& \=$\neg$($x$ when $e$) $=$ ($x$ after $e$) $\in$ $T$\+
\\[0ex]\& ($\forall$${\it e''}$:E. ($e$ $<$loc ${\it e''}$) $\Rightarrow$ ${\it e''}$ $\leq$ ${\it e'}$  $\Rightarrow$ ($x$ when ${\it e''}$) $=$ ($x$ when ${\it e'}$) $\in$ $T$))
\-\-\-
\end{tabbing}